grammar for the supported subset of CSL in IDDCSL

csl_input 	= 	csl_formula 
csl_forumula	=  	'P' cmp real '[' path_formula ']' 
			|unop '(' csl_formula')' 
			| '('csl_forumula')' binop '('csl_forumula')'
			| ap

path_formula 	= 	'('csl_forumula')' 'U' closed_interval '('csl_forumula')'
			| 'F' closed_interval '('csl_forumula')'
			| 'G' closed_interval '('csl_forumula')'
			| 'X' '('csl_forumula')'

closed_interval	=	'[' real ',' real ']'

unop		= '!'|'~'
binop		= '&&' | '*' | '||' | '->' | '<-' | '<->'

ap 		= 	PLACE cmp num 
			| true
			| false
cmp 		= '=' | '!='| '>=' | '>' | '<=' | '<' 
num		= natural number
real		= real number

PLACE must be a valid placename

In the current version the temporal operators U, F and G are supported only in their time bounded version.

___________________________________________________________________--

march 16, 2009
Martin Schwarick
ms@informatik.tu-cottbus.de